Termination Proof Script
Consider the TRS R consisting of the rewrite rules
|
| 1: |
|
top(free(x)) |
→ top(check(new(x))) |
| 2: |
|
new(free(x)) |
→ free(new(x)) |
| 3: |
|
old(free(x)) |
→ free(old(x)) |
| 4: |
|
new(serve) |
→ free(serve) |
| 5: |
|
old(serve) |
→ free(serve) |
| 6: |
|
check(free(x)) |
→ free(check(x)) |
| 7: |
|
check(new(x)) |
→ new(check(x)) |
| 8: |
|
check(old(x)) |
→ old(check(x)) |
| 9: |
|
check(old(x)) |
→ old(x) |
|
There are 10 dependency pairs:
|
| 10: |
|
TOP(free(x)) |
→ TOP(check(new(x))) |
| 11: |
|
TOP(free(x)) |
→ CHECK(new(x)) |
| 12: |
|
TOP(free(x)) |
→ NEW(x) |
| 13: |
|
NEW(free(x)) |
→ NEW(x) |
| 14: |
|
OLD(free(x)) |
→ OLD(x) |
| 15: |
|
CHECK(free(x)) |
→ CHECK(x) |
| 16: |
|
CHECK(new(x)) |
→ NEW(check(x)) |
| 17: |
|
CHECK(new(x)) |
→ CHECK(x) |
| 18: |
|
CHECK(old(x)) |
→ OLD(check(x)) |
| 19: |
|
CHECK(old(x)) |
→ CHECK(x) |
|
The approximated dependency graph contains 4 SCCs:
{13},
{14},
{15,17,19}
and {10}.
-
Consider the SCC {13}.
There are no usable rules.
By taking the AF π with
π(NEW) = 1 together with
the lexicographic path order with
empty precedence,
rule 13
is strictly decreasing.
-
Consider the SCC {14}.
There are no usable rules.
By taking the AF π with
π(OLD) = 1 together with
the lexicographic path order with
empty precedence,
rule 14
is strictly decreasing.
-
Consider the SCC {15,17,19}.
There are no usable rules.
By taking the AF π with
π(CHECK) = π(free) = π(new) = 1 together with
the lexicographic path order with
empty precedence,
the rules in {15,17}
are weakly decreasing and
rule 19
is strictly decreasing.
There is one new SCC.
-
Consider the SCC {15,17}.
By taking the AF π with
π(CHECK) = π(free) = 1 together with
the lexicographic path order with
empty precedence,
rule 15
is weakly decreasing and
rule 17
is strictly decreasing.
There is one new SCC.
-
Consider the SCC {15}.
By taking the AF π with
π(CHECK) = 1 together with
the lexicographic path order with
empty precedence,
rule 15
is strictly decreasing.
-
Consider the SCC {10}.
The usable rules are {2-9}.
The constraints could not be solved.
Tyrolean Termination Tool (0.05 seconds)
--- May 4, 2006